Nuprl Definition : Rpre 0,22
@loc precondition for a(v:T):
@loc P State(ds) v
== inr(inr(inr(inr(inr(inr(inr(inl(<loc,ds,a,T,P>)))))))) 
latex

Definitionsinr(x), inl(x), <a,b>
FDL editor aliasesRpre

origin